import Mathlib

open Filter
open scoped Topology

namespace CNVSAsymptoticKnowledge

/--
Modello asintotico della restrizione di conoscenza.
-/
structure AsymptoticKnowledgeModel where
  Verifier : Type
  Time : Type

  KVerifier : Verifier → Time → ℝ
  IGlobal : ℕ → ℝ

  Kmax : ℝ

  knowledge_nonnegative :
    ∀ j t, 0 ≤ KVerifier j t

  knowledge_bounded :
    ∀ j t, KVerifier j t ≤ Kmax

  global_information_positive :
    ∀ n, 0 < IGlobal n

  global_information_tendsto_infty :
    Tendsto IGlobal atTop atTop

/-- Rapporto locale/globale di conoscenza. -/
noncomputable def asymptoticKnowledgeRatio
    (M : AsymptoticKnowledgeModel)
    (j : M.Verifier)
    (t : M.Time)
    (n : ℕ) : ℝ :=
  M.KVerifier j t / M.IGlobal n

/--
Lemma analitico:
se `I(n) → +∞`, allora `K / I(n) → 0`.
-/
theorem constant_div_tendsto_zero
    (K : ℝ)
    (I : ℕ → ℝ)
    (hI : Tendsto I atTop atTop) :
    Tendsto (fun n : ℕ => K / I n) atTop (𝓝 0) := by
  have hInv :
      Tendsto (fun n : ℕ => (I n)⁻¹) atTop (𝓝 0) := by
    exact tendsto_inv_atTop_zero.comp hI
  simpa [div_eq_mul_inv] using
    (tendsto_const_nhds.mul hInv)

/--
Knowledge Restriction Principle, forma asintotica del bound superiore.

Se l'informazione globale tende a infinito, allora:

  Kmax / IGlobal(n) → 0
-/
theorem knowledge_restriction_asymptotic_bound
    (M : AsymptoticKnowledgeModel) :
    Tendsto
      (fun n : ℕ => M.Kmax / M.IGlobal n)
      atTop
      (𝓝 0) := by
  exact constant_div_tendsto_zero
    M.Kmax
    M.IGlobal
    M.global_information_tendsto_infty

/--
Esempio concreto:
Kmax = 10
IGlobal(n) = n + 1

Allora 10 / (n + 1) → 0.
-/
example :
    Tendsto
      (fun n : ℕ => 10 / ((n : ℝ) + 1))
      atTop
      (𝓝 0) := by
  have h :
      Tendsto (fun n : ℕ => (n : ℝ)) atTop atTop := by
    exact tendsto_natCast_atTop_atTop
  have hplus :
      Tendsto (fun n : ℕ => (n : ℝ) + 1) atTop atTop := by
    exact tendsto_atTop_add_const_right atTop 1 h
  exact constant_div_tendsto_zero 10
    (fun n : ℕ => (n : ℝ) + 1)
    hplus

end CNVSAsymptoticKnowledge